*****ASSUME ∃z.(R(x,y,z)∧E(z,v,w));

1 ∃z.(R(x,y,z)∧E(z,v,w))  (1)

*****ASSUME R(x,y,z);

2 R(x,y,z)  (2)

*****∃E ↑↑ z1;

3 R(x,y,z1)∧E(z1,v,w)  (3)

*****∀E foo2 x,y,z,z1;

4 (R(x,y,z)∧R(x,y,z1))⊃z=z1  

*****TAUTEQ E(z,v,w) 2:4;

5 E(z,v,w)  (1 2)

*****⊃I 2⊃↑;

6 R(x,y,z)⊃E(z,v,w)  (1)

*****∀I ↑ z;

7 ∀z.(R(x,y,z)⊃E(z,v,w))  (1)

*****⊃I 1⊃↑;

8 ∃z.(R(x,y,z)∧E(z,v,w))⊃∀z.(R(x,y,z)⊃E(z,v,w))  

*****ASSUME ∀z.(R(x,y,z)⊃E(z,v,w));

9 ∀z.(R(x,y,z)⊃E(z,v,w))  (9)

*****∀E foo1 x,y;

10 ∃z.R(x,y,z)  

*****∃E ↑ z1;

11 R(x,y,z1)  (11)

*****∀E ↑↑↑ z1;

12 R(x,y,z1)⊃E(z1,v,w)  (9)

*****TAUT R(x,y,z1)∧E(z1,v,w) 11:12;

13 R(x,y,z1)∧E(z1,v,w)  (9 11)

*****∃I ↑ z1 ;

14 ∃z1.(R(x,y,z1)∧E(z1,v,w))  (9)

*****⊃I 9⊃↑;

15 ∀z.(R(x,y,z)⊃E(z,v,w))⊃∃z1.(R(x,y,z1)∧E(z1,v,w))  

*****TAUT ∀z.(R(x,y,z)⊃E(z,v,w))≡∃z1.(R(x,y,z1)∧E(z1,v,w)) 8,15;

16 ∀z.(R(x,y,z)⊃E(z,v,w))≡∃z1.(R(x,y,z1)∧E(z1,v,w))